|
課程名稱 |
軟體規格與驗證
Software Specification and Verification |
|
開課學期 |
111-1 |
|
授課對象 |
管理學院 資訊管理學系 |
|
授課教師 |
蔡益坤 |
|
課號 |
IM7079 |
|
課程識別碼 |
725 U3220 |
|
班次 |
|
|
學分 |
3.0 |
|
全/半年 |
半年 |
|
必/選修 |
選修 |
|
上課時間 |
星期三7,8,9(14:20~17:20) |
|
上課地點 |
管一203 |
|
備註 |
總人數上限：20人
外系人數限制：8人 |
|
|
|
|
課程簡介影片 |
|
|
核心能力關聯 |
核心能力與課程規劃關聯圖 |
|
課程大綱
|
|
為確保您我的權利,請尊重智慧財產權及不得非法影印
|
|
課程概述 |
This is an introductory course on formal software specification and verification, covering various formalisms, methods, and tools for specifying the properties of a software program and for verifying that the program meets its specification. We will focus on deductive (theorem proving) methods. A separate, complementary course entitled “Automatic Verification” covers algorithmic (model checking) methods. |
|
課程目標 |
The goal of this course is to acquaint the students with fundamentals of formal software verification and to prepare them for conducting research in the area. |
|
課程要求 |
Computer Programming and Discrete Mathematics |
|
預期每週課後學習時數 |
About 6 hours |
|
Office Hours |
每週三 13:30~14:00
每週二 13:30~14:00 備註： Or by appointment, in Room 1108 of Management Building 2. |
|
指定閱讀 |
Class Notes and Selected Readings |
|
參考書目 |
Logic for Computer Science: Foundations of Automatic Theorem Proving, J.H. Gallier, Harper & Row Publishers, 1985.
Proof Theory and Automated Deduction, J. Goubault-Larrecq and I. Mackie, Kluwer Academic Publishers, 1997.
Logic in Computer Science: Modelling and Reasoning about Systems, M. Huth and M. Ryan, Cambridge University Press, 2004.
Foundations for Programming Languages, J.C. Mitchell, The MIT Press, 1996.
Formal Syntax and Semantics of Programming Languages, K. Slonneger and B.L. Kurtz, Addison-Wesley, 1995.
Verification of Sequential and Concurrent Programs, 2nd Edition, K.R. Apt and E.-R. Olderog, Springer-Verlag, 1997.
The Science of Programming, D. Gries, Springer-Verlag, 1981.
Predicate Calculus and Program Semantics, E.W. Dijkstra and C.S. Scholten, Springer-Verlag, 1990.
Programming from Specifications, 2nd Edition, C. Morgan, 1994.
Introduction to C program proof with Frama-C and its WP plugin, Allan Blanchard, 2020.
Software Foundations, B.C. Pierce, C. Casinghino, M. Greenberg, V. Sjoberg, and B. Yorgey.
Certified Programming with Dependent Types , A. Chilipala.
The Z Notation: A Reference Manual, 2nd Edition, J.M. Spivey, 1992.
Software Engineering with B, J.B. Wordsworth, Addison-Wesley, 1996.
Modeling in Event-B: System and Software Engineering, J.-R. Abrial, Cambridge University Press, 2010.
The Temporal Logic of Reactive and Concurrent Systems: Specification, Z. Manna and A. Pnueli, Springer-Verlag, 1992.
Temporal Verification of Reactive Systems: Safety, Z. Manna and A. Pnueli, Springer, 1995.
Temporal Verification of Reactive Systems: Progress, Z. Manna and A. Pnueli, Book Draft, 1996.
Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers, L. Lamport, Addison-Wesley, 2003.
Parallel Program Design: A Foundation, K.M. Chandy and J. Misra, Addison-Wesley, 1988.
A Discipline of Multiprogramming: Programming Theory for Distributed Applications, J. Misra, Springer, 2001
Beauty Is Our Business: A Birthday Salute to Edsger W. Dijkstra, Edited by W.H.J. Feijen, A.J.M. van Gasteren, D. Gries, and J. Misra, Springer-Verlag, 1990
The Formal Methods Page: http://formalmethods.wikia.com/wiki/Formal_methods, J. Bowen. (Note: this Web portal provides links to numerous formal methods and tools.) |
|
評量方式
(僅供參考) |
|
No. |
項目 |
百分比 |
說明 |
|
1. |
Homework Assignments |
20% |
There are six homework assignments. |
2. |
Participation |
10% |
The students are expected to attend all lectures and actively participate in discussions. |
3. |
Final Exam |
40% |
|
4. |
Term Report |
30% |
Report on the formal verification of a non-trivial program. |
|
|
針對學生困難提供學生調整方式 |
|
上課形式 |
以錄音輔助 |
|
作業繳交方式 |
延長作業繳交期限 |
|
考試形式 |
延後期末考試日期(時間) |
|
其他 |
由師生雙方議定 |
|
|
週次 |
日期 |
單元主題 |
|
第1週 |
9/7 |
Introduction: Reasoning about Programs; Fundamentals: Propositional and First-Order Logics |
|
第2週 |
9/14 |
Fundamentals: Propositional and First-Order Logics |
|
第3週 |
9/21 |
Fundamentals: Propositional and First-Order Logics |
|
第4週 |
9/28 |
Holiday; no class meeting |
|
第5週 |
10/5 |
Verification Tools: Coq |
|
第6週 |
10/12 |
Verification Tools: Coq |
|
第7週 |
10/19 |
Sequential Programs: Hoare Logic (I) |
|
第8週 |
10/26 |
Sequential Programs: Hoare Logic (I) |
|
第9週 |
11/2 |
Predicate Transformers |
|
第10週 |
11/9 |
Procedures: Hoare Logic (II) |
|
第11週 |
11/16 |
Verification Tools: Frama-C + Plugins |
|
第12週 |
11/23 |
Verification Tools: Frama-C + Plugins |
|
第13週 |
11/30 |
Concurrent, Reactive Systems: Owicki-Gries Method |
|
第14週 |
12/7 |
Concurrent, Reactive Systems: UNITY and Linear Temporal Logic |
|
第15週 |
12/14 |
Selected Topics: Modular/Compositional Reasoning |
|
第16週 |
12/21 |
Final Exam |
|